basic
\\[0ex]FunThru2op($A$;$B$;${\it opa}$;${\it opb}$;$f$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$a_{1}$, $a_{2}$:$A$. $f$($a_{1}$ ${\it opa}$ $a_{2}$) = (($f$($a_{1}$)) ${\it opb}$ ($f$($a_{2}$)))